A:Type, L:(A List), n:. (n  ||L||)  (lastn(n;L)  (A List)) 

latex

ProofTree

Definitions	Type, t  T, s = t, type List, , x:AB(x), x:A. B(x), ||as||, {x:A| B(x)} , , |g|, S  T, A  B, n - m, nth_tl(n;as), P  Q, lastn(n;L)
Lemmas	nth tl wf, le wf, length wf1, nat wf